pwd
cd 'JRWG-World:JRWG-Data:Research:Papers:97 Abs TCS:'

ls .tex
atoe-tcsA.tex
atoe-tcsB.tex
atoe-tcsC.tex
atoe-tcsD.tex
atoe-tcsJE.tex
atoe-tcsJF.tex
atoe-tcsJG.tex
atoe-tcsJH.tex
atoe-tcsJI.tex
atoe-tcsZ.tex
atoe-tcsZB.tex
atoe-tcsZC.tex


compare atoe-tcsJF.tex atoe-tcsZ.tex

compare atoe-tcsZ.tex atoe-tcsJG.tex

compare atoe-tcsJH.tex atoe-tcsJG.tex > DiffsJGtoJH

setfile -C unix DiffsJGtoJH

compare atoe-tcsJH.tex atoe-tcsJI.tex

File #1: atoe-tcsJH.tex
File #2: atoe-tcsJI.tex

Nonmatching lines (File "atoe-tcsJH.tex"; Line 2932; File "atoe-tcsJI.tex"; Line 2932)
2932	follow immediately from Weak Acyclicity Lemma and Stability Lemma,

2932	follow immediately from the Weak Acyclicity Lemma and the Stability Lemma,


Nonmatching lines (File "atoe-tcsJH.tex"; Line 3013:3016; File "atoe-tcsJI.tex"; Line 3013:3017)
3013	$\lin\stab$-needed reductions in $\lin\calF$, which are actually
3014	$\lin\stab$-needed complete family-reductions by
3015	\Lr{L.aff.un.f.l.}.(4) and \Tr{T.line.zig.}, and hence are optimal w.r.t.
3016	$\lin\stab$, implement optimal family-reductions in $\calF$, w.r.t~$\stab$.

3013	$\lin\stab$-needed reductions in $\lin\calF$ are actually
3014	$\lin\stab$-needed complete family-reductions by
3015	\Lr{L.aff.un.f.l.}.(4) and \Tr{T.line.zig.}. Hence
3016	$\lin\stab$-needed reductions are optimal w.r.t.
3017	$\lin\stab$ and implement optimal family-reductions in $\calF$, w.r.t~$\stab$.


*** EOF on both files at the same time ***

compare atoe-tcsJI.tex atoe-tcsZB.tex

compare atoe-tcsZB.tex atoe-tcsZC.tex

compare atoe-tcsZB.tex atoe-tcsJJ.tex
File #1: atoe-tcsZB.tex
File #2: atoe-tcsJJ.tex

Nonmatching lines (File "atoe-tcsZB.tex"; Line 64:65; File "atoe-tcsJJ.tex"; Line 64:66)
  64	\newcommand{\john}[1]{\{{\bf John: \sf #1}\}} % Highlight text.
  65	\newcommand{\zurab}[1]{\{{\bf Zurab: \sf #1}\}} % Highlight text.

  64	\newcommand{\zurab}[1]{#1} % include text.
  65	\newcommand{\john}[1]{\{{\bf John: \sf #1}\}} % Highlight text.
  66	%\newcommand{\zurab}[1]{\{{\bf Zurab: \sf #1}\}} % Highlight text.


Extra lines in 2nd before 526 in 1st (File "atoe-tcsZB.tex"; Line 526; File "atoe-tcsJJ.tex"; Line 527:537)
 527	It should be remarked that it is not the aim of this paper to
 528	provide a comprehensive abstract theory of normalization and optimality
 529	that can readily be applied to particular (syntactic) systems covered by
 530	SDRSs and DFSs. In particular, it cannot replace the syntactic studies of
 531	normalization and optimality in the literature (part of which was mentioned
 532	above):  some of our axioms are non-trivial to verify for particular
 533	systems, and we do not cover all aspects of the subject. Rather, we try to
 534	bring out and analyze some of the main principles and methods on which the
 535	theory of normalization and optimality is based. And although our abstract
 536	framework is very general, our results and proofs are far from trivial and
 537	do save considerable work for particular systems.


Nonmatching lines (File "atoe-tcsZB.tex"; Line 1633:1634; File "atoe-tcsJJ.tex"; Line 1645)
1633	in a DFS ${\calF}$. Then any sequentialization of an $\stab$-needed
1634	family-reduction is weakly $\stab$-needed.

1645	in a DFS ${\calF}$. Then any sequentialization of an $\stab$-needed
		family-reduction is weakly $\stab$-needed.


Nonmatching lines (File "atoe-tcsZB.tex"; Line 2055:2058; File "atoe-tcsJJ.tex"; Line 2066:2069)
2055	extraction algorithm checks every standard variant of $P'$ in order to find
2056	one whose last step does not create $u'$ and therefore can be omitted. The
2057	following lemma says that we can indeed restrict our search to standard
2058	reductions only:

2066	extraction algorithm (when applied to $Pu$) checks every standard variant
2067	of $P$ in order to find one whose last step does not create $u$ and
2068	therefore can be omitted. The following lemma says that we can indeed
2069	restrict our search to standard reductions only:


Nonmatching lines (File "atoe-tcsZB.tex"; Line 2643; File "atoe-tcsJJ.tex"; Line 2654:2655)
2643	the proof of \Tr{T.sep.eq.ig.} (as well as
		in~\cite{[icalp],[mfcs]}).

2654	the proof of \Tr{T.sep.eq.ig.} (as well as
2655	in~\cite{[icalp],[icalp-rep],[mfcs]}).


Nonmatching lines (File "atoe-tcsZB.tex"; Line 2807:2808; File "atoe-tcsJJ.tex"; Line 2819:2820)
2807	parallel, is
2808	a complete family-reduction which is not a reduction, contradicting~(4).

2819	parallel, is
		a complete family-reduction which is not a reduction, contradicting~(4).


Nonmatching lines (File "atoe-tcsZB.tex"; Line 2870; File "atoe-tcsJJ.tex"; Line 2882)
2870	\item[\suf] ${\calF}=({\calR}, \sfami,\scontr)$ be separable, and suppose

2882	\item[\suf] Let ${\calF}=({\calR}, \sfami,\scontr)$ be separable, and suppose


Nonmatching lines (File "atoe-tcsZB.tex"; Line 2928; File "atoe-tcsJJ.tex"; Line 2940:2941)
2928	Let ${\calF}=({\calR},\fami,\contr)$ be a DFS. The \emph{implementation}

2940	Let ${\calF}=({\calR},\fami,\contr)$ be a DFS where $\calR=(A,/)$ and
2941	$A=(Ter,Red,\ar)$. Then the \emph{implementation}


Nonmatching lines (File "atoe-tcsZB.tex"; Line 2933:2944; File "atoe-tcsJJ.tex"; Line 2946:2956)
2933	underlying ARS $A$ of
2934	${\calR}_I=(A,/)$ are complete family-reductions starting from $t_\emp$,
2935	each edge (i.e., reduction step) being a multi-step contracting a family
2936	of
2937	redexes.
2938	
2939	\item[\labelitemi] the residual relation $/$ is defined as follows:
2940	let $U$ and $V$
2941	be complete sets of redexes in two families, in a term $s$, and let $U:s\ar
2942	o$ be the multi-step contracting $U$. Then $V/U$ is the multi-step $o\ar e$
2943	contracting all members of the set $V/U$.
2944	

2946	underlying ARS $A_I$ of
2947	${\calR}_I=(A_I,/_I)$ are complete family-reductions starting from
2948	$t_\emp$, each edge (i.e., reduction step) being a multi-step contracting a
2949	family of redexes.
2950	
2951	\item[\labelitemi] the residual relation $/_I$ is defined as follows:
2952	let $U$ and $V$ be complete sets of redexes in two $\fami$-families, in a
2953	term $s$, and let $U:s\ar_I o$ be the multi-step contracting $U$. Then
2954	$V/_I U$ is the multi-step $o\ar_I e$ contracting all members of the set
2955	$V/U$.
2956	


Nonmatching lines (File "atoe-tcsZB.tex"; Line 2978; File "atoe-tcsJJ.tex"; Line 2990)
2978	Thus the residual relation is well defined. Obviously, $V/V=\emp$, and

2990	Thus the residual relation is well defined. Obviously, $V/_I V=\emp$, and


Nonmatching lines (File "atoe-tcsZB.tex"; Line 2981; File "atoe-tcsJJ.tex"; Line 2993)
2981	follow immediately from the Weak Acyclicity Lemma and Stability Lemma,

2993	follow immediately from the Weak Acyclicity Lemma and the Stability Lemma,


Nonmatching lines (File "atoe-tcsZB.tex"; Line 3057:3058; File "atoe-tcsJJ.tex"; Line 3069:3070)
3057	The following lemma relates neededness in a DFSs with neededness in its
3058	implementation. Together with \Tr{T.unif.opt.}, it implies that the

3069	The following lemmas relate neededness in a DFSs with neededness in its
3070	implementation. Together with \Tr{T.unif.opt.}, they imply that the


Nonmatching lines (File "atoe-tcsZB.tex"; Line 3062:3063; File "atoe-tcsJJ.tex"; Line 3074:3075)
3062	$\lin\stab$-needed reductions in $\lin\calF$ are actually
3063	$\lin\stab$-needed complete family-reductions by

3074	$\lin\stab$ is stable and $\lin\stab$-needed reductions in $\lin\calF$ are
3075	actually $\lin\stab$-needed complete family-reductions by


Nonmatching lines (File "atoe-tcsZB.tex"; Line 3077; File "atoe-tcsJJ.tex"; Line 3089)
3077	Let $t\red{u} s$ in $\lin\calF$, where $t\not\in\lin\stab$ and

3089	Let $t\red{u}_I s$ in $\lin\calF$, where $t\not\in\lin\stab$ and


Nonmatching lines (File "atoe-tcsZB.tex"; Line 3095:3096; File "atoe-tcsJJ.tex"; Line 3107:3109)
3095	$P_I:t_0\red{u_0}t_1\red{u_1}\ldots \ar t_n$ be its corresponding reduction
3096	in $\lin\calF$. Then $P$ is $\stab$-needed iff $P_I$ is $\lin\stab$-needed.

3107	$P_I:t_0\red{u_0}_I t_1\red{u_1}_I\ldots \ar_I t_n$ be its corresponding
3108	reduction in $\lin\calF$. Then $P$ is $\stab$-needed iff $P_I$ is
3109	$\lin\stab$-needed.


Nonmatching lines (File "atoe-tcsZB.tex"; Line 3102; File "atoe-tcsJJ.tex"; Line 3115)
3102	some $i$. Then there is an $\lin\stab$-normalizing reduction $N:t_i\doar s$

3115	some $i$. Then there is an $\lin\stab$-normalizing reduction $N:t_i\doar_I s$


Nonmatching lines (File "atoe-tcsZB.tex"; Line 3195; File "atoe-tcsJJ.tex"; Line 3208)
3195	in~\cite{[icalp]} we studied the concepts of \emph{independence} and

3208	in~\cite{[icalp],[icalp-rep]} we studied the concepts of \emph{independence} and


Nonmatching lines (File "atoe-tcsZB.tex"; Line 3198:3207; File "atoe-tcsJJ.tex"; Line 3211:3221)
3198	orthogonal rewrite systems. And we have also developed a relativized
3199	computational semantics for orthogonal reduction systems~\cite{[mfcs]},
3200	extending the computational semantics of rewrite systems proposed
3201	by Boudol~\cite{[Bou]}. Among (many other) possible directions for future
3202	work, let us mention that it is important to extend these results,
3203	especially the semantic part, to non-deterministic systems, to enable one
3204	to model for example languages for concurrency as well.
3205	
3206	
3207	

3211	orthogonal rewrite systems. And we have also developed a relativized stable
3212	computational semantics for orthogonal reduction systems~\cite{[stable]},
3213	extending the computational semantics of rewrite systems proposed
3214	by Boudol~\cite{[Bou]}. \zurab{Among (many other) possible directions for future
3215	work, let us mention that it is important to extend these results,
3216	both the syntactic and semantic parts, to non-deterministic systems, to
3217	enable one to model for example languages for concurrency as well. Related
3218	work in this direction (not restricted to conflict-free systems)
3219	includes~\cite{[Bou],[C.K.],[Raa.th],[Mel.th],[Mel2],[Mel98]}.}
3220	
3221	


Extra lines in 2nd before 3295 in 1st (File "atoe-tcsZB.tex"; Line 3295; File "atoe-tcsJJ.tex"; Line 3309:3315)
3309	
3310	\bibitem{[C.K.]}
3311	D. Clark and J.R. Kennaway, Event structures and non-orthogonal term graph
3312	rewriting, \emph{Mathematical Structures in Computer Science} {\bf 6}
3313	(1996) 545-578.
3314	
3315	


Nonmatching lines (File "atoe-tcsZB.tex"; Line 3412:3413; File "atoe-tcsJJ.tex"; Line 3433)
3412	Computation}
3413	{\bf 119(1)} (1995) 18-38.

3433	Computation}
		{\bf 119(1)} (1995) 18-38.


Nonmatching lines (File "atoe-tcsZB.tex"; Line 3433:3435; File "atoe-tcsJJ.tex"; Line 3453:3455)
3433	\bibitem{[mfcs98]}
3434	Z. Khasidashvili, Stable computational semantics of conflict-free rewrite
3435	systems. (Submitted.)

3453	\bibitem{[stable]}
3454	Z. Khasidashvili, Stable computational semantics of conflict-free rewrite
3455	systems. (Draft.)


Extra lines in 2nd before 3463 in 1st (File "atoe-tcsZB.tex"; Line 3463; File "atoe-tcsJJ.tex"; Line 3483:3488)
3483	\bibitem{[icalp-rep]}
3484	Z. Khasidashvili and J.R.W. Glauert, The geometry of conflict-free
3485	reduction spaces,  Technical Report
3486	SYS-C98-04, UEA Norwich,~1998.
3487	
3488	


Nonmatching lines (File "atoe-tcsZB.tex"; Line 3499:3500; File "atoe-tcsJJ.tex"; Line 3525)
3499	Th\`ese
3500	de l'Universit\'e de Paris VII, 1978.

3525	Th\`ese
		de l'Universit\'e de Paris VII, 1978.


Extra lines in 2nd before 3525 in 1st (File "atoe-tcsZB.tex"; Line 3525; File "atoe-tcsJJ.tex"; Line 3550:3558)
3550	\bibitem{[Mel2]}
3551	P.-A. Melli\`es, Axiomatic rewriting theory II: The lambda-sigma-calculus
3552	has the finite cone property, submitted.
3553	
3554	\bibitem{[Mel98]}
3555	P.-A. Melli\`es, Axiomatic rewriting theory IV: A stability theorem in
3556	rewriting theory, in: \emph{Proc. 14th IEEE Symp. on Logic in Computer
3557	Science} (1998).
3558	


Extra lines in 2nd before 3569 in 1st (File "atoe-tcsZB.tex"; Line 3569; File "atoe-tcsJJ.tex"; Line 3603:3604)
3603	
3604	


*** EOF on both files at the same time ***



compare atoe-tcsZC.tex atoe-tcsJJ.tex
File #1: atoe-tcsZC.tex
File #2: atoe-tcsJJ.tex

Extra lines in 1st before 62 in 2nd (File "atoe-tcsZC.tex"; Line 62:67; File "atoe-tcsJJ.tex"; Line 62)
  62	%\newcommand{\john}[1]{} % Comment out text.
  63	%\newcommand{\zurab}[1]{} % Comment out text.
  64	\newcommand{\zurab}[1]{#1} % include text.
  65	\newcommand{\john}[1]{\{{\bf John: \sf #1}\}} % Highlight text.
  66	%\newcommand{\zurab}[1]{\{{\bf Zurab: \sf #1}\}} % Highlight text.
  67	\newcommand{\delete}[1]{} % Comment out text.


Extra lines in 1st before 66 in 2nd (File "atoe-tcsZC.tex"; Line 72:73; File "atoe-tcsJJ.tex"; Line 66)
  72	\newcommand{\excl}[1]{} % exclude text.
  73	%\newcommand{\excl}[1]{\{#1\}} % include text.


Nonmatching lines (File "atoe-tcsZC.tex"; Line 527; File "atoe-tcsJJ.tex"; Line 519)
 527	\zurab{It should be remarked that it is not the aim of this paper to

 519	It should be remarked that it is not the aim of this paper to


Nonmatching lines (File "atoe-tcsZC.tex"; Line 530; File "atoe-tcsJJ.tex"; Line 522)
 530	SDRSs and DFSs.  In particular, it cannot replace the syntactic studies of

 522	SDRSs and DFSs. In particular, it cannot replace the syntactic studies of


Nonmatching lines (File "atoe-tcsZC.tex"; Line 536:538; File "atoe-tcsJJ.tex"; Line 528:529)
 536	framework is very general, our results and proofs are far non-trivial and
 537	do save much work for particular systems.
 538	}

 528	framework is very general, our results and proofs are far from trivial and
 529	do save considerable work for particular systems.


Nonmatching lines (File "atoe-tcsZC.tex"; Line 825; File "atoe-tcsJJ.tex"; Line 816)
 825	different). Thus \delete{by \Pr{L.perm.equiv.}.(3),} $v_i/Q_i\cap

 816	different). Thus \suppress{by \Pr{L.perm.equiv.}.(3),} $v_i/Q_i\cap


Nonmatching lines (File "atoe-tcsZC.tex"; Line 1156; File "atoe-tcsJJ.tex"; Line 1147)
1156	\delete{\Cr{T.4.1.}} \Lr{L.4.4.}.(1), there is an $\reg$-needed

1147	\suppress{\Cr{T.4.1.}} \Lr{L.4.4.}.(1), there is an $\reg$-needed


Nonmatching lines (File "atoe-tcsZC.tex"; Line 1455; File "atoe-tcsJJ.tex"; Line 1446)
1455	\delete{(see Figure~\ref{elem-diag})} By axioms [creation] and

1446	\suppress{(see Figure~\ref{elem-diag})} By axioms [creation] and


Nonmatching lines (File "atoe-tcsZC.tex"; Line 1578; File "atoe-tcsJJ.tex"; Line 1569)
1578	of \delete{\Cr{T.4.1.}} \Lr{L.4.4.}.

1569	of \suppress{\Cr{T.4.1.}} \Lr{L.4.4.}.


Nonmatching lines (File "atoe-tcsZC.tex"; Line 2503:2505; File "atoe-tcsJJ.tex"; Line 2494:2496)
2503	Below, $FAM_z(P)$ \excl{(resp. $SFAM_z(P)$)} denotes the set of zig-zag
2504	classes whose
2505	\excl{(resp. $P$-needed)} member redexes are contracted in $P$, in an ASDRS; and

2494	Below, $FAM_z(P)$ \suppress{(resp. $SFAM_z(P)$)} denotes the set of zig-zag
2495	classes whose
2496	\suppress{(resp. $P$-needed)} member redexes are contracted in $P$, in an ASDRS; and


Nonmatching lines (File "atoe-tcsZC.tex"; Line 2513:2514; File "atoe-tcsJJ.tex"; Line 2504:2505)
2513	If $Pv\zfami Qw$, then $v/(Q/P)=w/(P/Q)$. In particular, if $P\staeq Q$,
2514	then $v=w$.

2504	If $Pv\zfami Qw$, then $v/(Q/P)=w/(P/Q)$. In particular,
2505	where $P\staeq Q$, it follows that $v=w$.


Nonmatching lines (File "atoe-tcsZC.tex"; Line 2652; File "atoe-tcsJJ.tex"; Line 2643)
2652	\excl{

2643	\suppress{


Nonmatching lines (File "atoe-tcsZC.tex"; Line 2893; File "atoe-tcsJJ.tex"; Line 2884)
2893	\excl{\Pr{P.leqv.sam.se.es.fa.}.(1)} \incl{\Lr{L.sta.eq.sa.fam.}} that

2884	\suppress{\Pr{P.leqv.sam.se.es.fa.}.(1)} \incl{\Lr{L.sta.eq.sa.fam.}} that


Nonmatching lines (File "atoe-tcsZC.tex"; Line 2994; File "atoe-tcsJJ.tex"; Line 2985)
2994	follow immediately from the Weak Acyclicity Lemma and Stability Lemma,

2985	follow immediately from the Weak Acyclicity Lemma and the Stability Lemma,


Nonmatching lines (File "atoe-tcsZC.tex"; Line 3215:3220; File "atoe-tcsJJ.tex"; Line 3206:3211)
3215	by Boudol~\cite{[Bou]}. \zurab{Among (many other) possible directions for future
3216	work, let us mention that it is important to extend these results,
3217	both the syntactic and semantic parts, to non-deterministic systems, to
3218	enable one to model for example languages for concurrency as well. Related
3219	work in this direction (not restricted to conflict-free systems)
3220	includes~\cite{[Bou],[C.K.],[Raa.th],[Mel.th],[Mel2],[Mel98]}.}

3206	by Boudol~\cite{[Bou]}. Among many possible directions for future
3207	work, let us mention that it is important to extend these results,
3208	both the syntactic and semantic aspects, to non-deterministic systems,
3209	enabling one to model languages for concurrency for example. Related
3210	work in this direction (not restricted to conflict-free systems)
3211	includes~\cite{[Bou],[C.K.],[Raa.th],[Mel.th],[Mel2],[Mel98]}.


Nonmatching lines (File "atoe-tcsZC.tex"; Line 3225; File "atoe-tcsJJ.tex"; Line 3216)
3225	\delete{

3216	\suppress{


Nonmatching lines (File "atoe-tcsZC.tex"; Line 3322; File "atoe-tcsJJ.tex"; Line 3313)
3322	\delete{

3313	\suppress{


Nonmatching lines (File "atoe-tcsZC.tex"; Line 3610; File "atoe-tcsJJ.tex"; Line 3601)
3610	\delete{

3601	\suppress{


Extra lines in 1st file (File "atoe-tcsZC.tex"; Line 3654:3662; File "atoe-tcsJJ.tex"; Line 3644)
3654	
3655	
3656	
3657	
3658	
3659	
3660	
3661	
3662	

*** EOF on both files ***

